#include "synthesis.h"
#include "debug.h"
#include "ltlf2dfa/synthesis.h"
#include "ltlfsyn/synthesis.h"
#include "synutil/formula_in_bdd.h"
#include "synutil/partvar.h"
#include "synutil/syn_states.h"
#include <numeric>
#include <vector>

Synthesis::Synthesis(aalta::aalta_formula *src_formula, std::unordered_set<std::string> &env_var, std::string partfile, bool verbose)
    : src_formula(src_formula), env_var(env_var), partfile(partfile), verbose(verbose)
{
    clear_XY_vars();
    ltlfsyn::PartitionAtoms(src_formula, env_var);
    // number of variables
    calc_XY_var_nums();

    FormulaInBdd::InitBdd4LTLf(src_formula);
    syn_states::insert_swin_state(FormulaInBdd::TRUE_bddP_);
    syn_states::insert_ewin_state(FormulaInBdd::FALSE_bddP_);

    hash_set<aalta_formula *> and_sub_afs_set = src_formula->and_to_set();
    and_sub_afs_vec.assign(and_sub_afs_set.begin(), and_sub_afs_set.end());
}

bool Synthesis::is_realizable()
{
    if (!preCheck_subAfs())
        return false;
    if (and_sub_afs_vec.size() == 1)
        return true;
    bool comp_syn_res = compositional_synthesis();
    return comp_syn_res;
}

/**
 * check realizability of each sub_afs, by forward search in JACM paper
 */
bool Synthesis::preCheck_subAfs()
{
    for (auto it : and_sub_afs_vec)
    {
        ltlfsyn::Syn_Frame *init = new ltlfsyn::Syn_Frame(it);
        if (!ltlfsyn::forwardSearch(init))
            return false;
    }
    return true;
}

// prepare for export DFA
void Synthesis::init_forDFA()
{
    var_num = total_var_nums;
    var_names.resize(total_var_nums);
    for (auto item : X_vars)
        var_names[item - 12] = aalta_formula(item, NULL, NULL).to_string();
    for (auto item : Y_vars)
        var_names[item - 12] = aalta_formula(item, NULL, NULL).to_string();
    orders.assign(var_num, 2);
    var_index.resize(var_num);
    indicies.resize(var_num);
    for (int i = 0; i < var_num; i++)
    {
        var_index[i] = i;
        indicies[i] = i;
    }
}

/**
 * compositional method
 */
bool Synthesis::compositional_synthesis()
{
    whole_dfa::SAT_TRACE_FLAG = false;
    syn_states::set_isAcc_byEmpty(FormulaInBdd::TRUE_bddP_, true);
    syn_states::set_isAcc_byEmpty(FormulaInBdd::FALSE_bddP_, false);
    init_forDFA();

    dexec(system("mkdir -p examples/temp-drafts"));
    const string REL_FOLDERNAME = "examples/temp-drafts/";
    // get whole DFA
    bool Minimize_FLAG = true;
    DFA *tmp_whole_dfa = dfaTrue(), *dfa_prev = NULL, *dfa_cur = NULL, *dfa_cur_merged = NULL;
    for (auto it : and_sub_afs_vec)
    {
        string af_s_whole = it->to_string();
        af_s_whole.erase(remove(af_s_whole.begin(), af_s_whole.end(), ' '), af_s_whole.end()); // delete all spaces from af_s
        const string REL_BASENAME = REL_FOLDERNAME + af_s_whole.substr(0, 30);
        Syn_Graph graph;
        my_dfaAssign(dfa_prev, tmp_whole_dfa);
        printDotAndDfaFile_forDebug(dfa_prev, REL_BASENAME + "_prev");

        whole_dfa::Syn_Frame *init = new whole_dfa::Syn_Frame(it);
        DdNode *init_bddP = init->GetBddPointer();
        dout << "sub_af:\t" << af_s_whole << endl;
        whole_dfa::search_whole_DFA(init, graph);
        dexec(printGraph(graph));

        dfa_cur = graph2DFA(graph, init_bddP, var_num, indicies);
        printDotAndDfaFile_forDebug(dfa_cur, REL_BASENAME + "_cur");
        Minimize_FLAG && (dfa_cur = my_dfaMinimize(dfa_cur));
        printDotAndDfaFile_forDebug(dfa_cur, REL_BASENAME + "_curMin");
        dfa_cur_merged = my_dfaProduct(dfa_prev, dfa_cur, dfaAND);
        printDotAndDfaFile_forDebug(dfa_cur_merged, REL_BASENAME + "_merged");
        Minimize_FLAG && (dfa_cur_merged = my_dfaMinimize(dfa_cur_merged));
        printDotAndDfaFile_forDebug(dfa_cur_merged, REL_BASENAME + "_mergedMin");
        bool dfa_syn_res = check_DFA_realizability(dfa_cur_merged);
        if (!dfa_syn_res)
            return false;
        my_dfaAssign(tmp_whole_dfa, dfa_cur_merged);
    }
    DFA *wholeDFA = NULL;
    my_dfaAssign(wholeDFA, tmp_whole_dfa);
    printDotAndDfaFile_forDebug(wholeDFA, REL_FOLDERNAME + "whole");
    bool wholeDFA_syn_res = check_DFA_realizability(wholeDFA);
    return wholeDFA_syn_res;
}